This invention relates to computer aided circuit design.
A circuit may be described as a set of definitions, with each definition specifying a gate of the circuit. For most circuits, the induced dependency graph of such a set of definitions is acyclic. That is, the circuit contains no feedback loops (without clocked delay elements) which may cause uncertainty in the state that the system must take on or, indeed, may cause the circuit to not settle to any stable state. In reviewing the set of definitions that together define a circuit, an individual definition or (more typically) a collection of definitions may be found to be semantically cyclic, or syntactically cyclic. A definition is syntactically cyclic when a variable p is expressed in terms of itself, or in terms of at least one other variable, q, that is effectively expressed in terms of p. A semantically cyclic definition is one that, for at least one valuation (e.g. with a specific valuation of one or more external variables of the circuit), a syntactically acyclic condition does not exist.
Syntactic cyclic definitions occur in many contexts in digital designs. S. Malik in xe2x80x9cAnalysis of cyclic combinational circuitsxe2x80x9d, IEEE Transactions on Computer-Aided Design, 1994, points out that it is often desirable to re-use functional units by connecting them in cyclic fashion through a routing mechanism, and L. Stok in xe2x80x9cFalse loops through resource sharingxe2x80x9d, in International Conference on Computer-Aided Design, 1992, notes that such definitions often arise in the output of synthesis programs. In these cases, the intention is that the routing mechanisms can be controlled through external inputs, so that any xe2x80x9csemanticallyxe2x80x9d cyclic paths are broken for each valuation of the external xe2x80x9cfreexe2x80x9d inputs and clocked delay elements (such as clocked latches).
Semantically cyclic definitions may, for example, occur inadvertently in systems composed of several Mealy machines, from feedback connections between the combinational inputs and outputs.
Verification systems that accept semantically cyclic definitions obviously run the risk of certifying systems that have the unacceptable behavior associated with a cyclic condition. On the other hand, verification systems that prohibit syntactically cyclic definitions reject circuit definitions that might be certified by formal verification as being free from cyclic conditions. Most current design and verification systems either prohibit all syntactically cyclic definitions, or accept only some of the semantically acyclic definitions that could be accepted.
The Esterel compiler appears to be the only known existing system that analyzes definitions for semantic cyclicity, using the notion of xe2x80x9cconstructivityxe2x80x9d proposed by Berry, The Constrictive Semantics of Esterel, Draft book, available at ftp://ftp-sop.inria.fr/meije/esterel/papers/constructiveness.ps.gz, 1995, which considers a circuit to be semantically acyclic iff for every external input, a unique value can be derived for each internal wire by a series of inferences on the definition of the circuit (a more precise statement is given below). T. Shiple, xe2x80x9cFormal Analysis of Synchronous Circuitsxe2x80x9d, PhD dissertation, University of California, Berkeley, 1996, shows that constructive definitions are precisely those that are well-behaved electrically, for any assignment of delay values, in the up-unbounded inertial delay model defined in by J. A. Brzozowski and C-J. H. Seger in xe2x80x9cAsynchronous Circuitsxe2x80x9d, Springer Verlag, 1994.
The work most related to this disclosure is described in the aforementioned Berry article and the aforementioned Shiple dissertation. Berry proposed the original operational formulation of constructivity (Constructivity) and the computational formulation (Constructivity-FIX), based on work by Malik""s aforementioned article. These definitions are based on computational processesxe2x80x94one would prefer a non-computational definition of the concept of xe2x80x9csemantic acyclicityxe2x80x9d. See also T. Shiple, G. Berry and H. Touati, xe2x80x9cConstructive analysis of cyclic circuitsxe2x80x9d, in European Design and Test Conference, 1996. The above references employ symbolic, fixpoint-based algorithms to check constructivity. These algorithms are difficult to implement and somewhat inefficient for variables with non-Boolean types.
It is inefficient to check constructivity by enumerating all possible external valuations. Symbolic algorithms for checking constructivity manipulate sets of input valuations, representing them with BDD""s. See R. Bryant, xe2x80x9cGraph based algorithms for boolean function manipulationxe2x80x9d, IEEE Transactions on Computers, 1986; and G. Berry, xe2x80x9cThe Constrictive Semantics of Esterelxe2x80x9d, Draft book, available at ftp://ftp-sop.inria.fr/meije/esterel/parers/constructiveness.ps.gz, 1995; the Shiple, G. Berry and H. Touati publication; and the Shiple PhD dissertation. This manipulation is based on simultaneous fixpoint equations derived from the circuit definitions and the types of the variables. For variables with k values in their type, these algorithms require k sets of valuations for each variable. Moreover, for arithmetic operations, the fixpoint equations are constructed from partitions (for +) or factorizations (for *) of all numbers in the type. Thus, these algorithms are somewhat inefficient and difficult to implement for variables with non-Boolean types.
The formulation disclosed herein overcomes the prior art limitations by presenting a simple, non-computational definition of constructivity (Constructivity-SAT) and a symbolic algorithm based on the new formulation that is simple to implement for variables with arbitrary finite types. It is shown that, by simple transformation, one can reformulate constructivity as the satisfiability of a set of equations derived from the definitions, over variable types extended with a value xe2x8axa5 (read as xe2x80x9cbottomxe2x80x9d). This formulation is non-computational and easily extensible to variables with any finite type. The formulation also handles definitions of indexed variables in the same manner. This constructivity check was implemented in COSPAN, which is the verification engine for the commercially available FormalCheck verification tool. The implementation is simple, and experience indicates that it usually incurs negligible overhead.